(0) Obligation:
Runtime Complexity TRS:
The TRS R consists of the following rules:
0(1(2(x1))) → 0(2(1(0(x1))))
0(1(2(x1))) → 1(0(2(3(x1))))
0(1(2(x1))) → 0(2(4(1(5(x1)))))
0(1(2(x1))) → 0(3(2(1(0(x1)))))
0(1(2(x1))) → 1(0(3(2(3(x1)))))
0(1(2(x1))) → 0(1(3(4(2(3(x1))))))
0(5(2(x1))) → 0(2(4(5(3(x1)))))
0(5(2(x1))) → 5(4(2(3(0(4(x1))))))
2(0(1(x1))) → 3(0(2(1(x1))))
2(0(1(x1))) → 0(2(1(1(4(x1)))))
2(0(1(x1))) → 0(3(2(4(1(x1)))))
2(0(1(x1))) → 3(0(2(1(4(x1)))))
2(0(1(x1))) → 0(2(2(3(4(1(x1))))))
2(0(1(x1))) → 0(3(2(3(1(1(x1))))))
2(0(1(x1))) → 4(0(4(2(1(4(x1))))))
2(5(1(x1))) → 0(2(1(5(1(x1)))))
2(5(1(x1))) → 1(4(5(4(2(x1)))))
2(5(1(x1))) → 5(0(2(1(4(x1)))))
2(5(1(x1))) → 5(2(1(4(1(x1)))))
2(5(1(x1))) → 1(5(0(2(4(1(x1))))))
2(5(1(x1))) → 5(2(1(1(1(1(x1))))))
0(1(2(1(x1)))) → 3(1(4(0(2(1(x1))))))
0(1(3(1(x1)))) → 5(0(3(1(1(x1)))))
0(1(3(1(x1)))) → 1(0(3(4(2(1(x1))))))
0(1(5(1(x1)))) → 5(0(3(1(1(x1)))))
0(2(1(2(x1)))) → 0(2(2(1(5(x1)))))
0(2(5(1(x1)))) → 1(1(5(0(2(1(x1))))))
0(5(3(1(x1)))) → 0(1(4(4(3(5(x1))))))
0(5(5(2(x1)))) → 5(4(2(3(5(0(x1))))))
2(0(1(2(x1)))) → 0(2(3(2(1(1(x1))))))
2(0(1(2(x1)))) → 4(0(2(1(1(2(x1))))))
2(0(4(1(x1)))) → 3(0(2(4(1(x1)))))
2(0(5(1(x1)))) → 5(4(2(1(0(x1)))))
2(2(5(1(x1)))) → 3(2(2(4(5(1(x1))))))
2(4(0(1(x1)))) → 1(0(2(4(4(x1)))))
2(4(0(1(x1)))) → 3(0(0(2(4(1(x1))))))
2(4(0(1(x1)))) → 5(4(0(2(1(1(x1))))))
2(5(2(1(x1)))) → 1(5(2(2(3(1(x1))))))
2(5(4(1(x1)))) → 4(5(2(1(4(4(x1))))))
2(5(5(1(x1)))) → 1(5(4(2(4(5(x1))))))
2(5(5(2(x1)))) → 5(5(2(3(2(x1)))))
0(1(3(0(1(x1))))) → 0(3(1(0(1(1(x1))))))
0(2(4(3(1(x1))))) → 1(3(4(2(3(0(x1))))))
0(2(4(3(1(x1))))) → 4(0(3(2(1(0(x1))))))
0(2(5(3(1(x1))))) → 5(0(2(3(5(1(x1))))))
2(0(5(4(1(x1))))) → 0(4(5(3(2(1(x1))))))
2(2(0(1(2(x1))))) → 2(4(0(2(2(1(x1))))))
2(4(0(5(1(x1))))) → 1(4(5(0(4(2(x1))))))
2(4(2(3(1(x1))))) → 4(2(2(3(3(1(x1))))))
2(5(2(0(1(x1))))) → 0(2(4(1(5(2(x1))))))
Rewrite Strategy: INNERMOST
(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)
Converted CpxTRS to CDT
(2) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
0'(1(2(z0))) → c(0'(2(1(0(z0)))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c1(0'(2(3(z0))), 2'(3(z0)))
0'(1(2(z0))) → c2(0'(2(4(1(5(z0))))), 2'(4(1(5(z0)))))
0'(1(2(z0))) → c3(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c4(0'(3(2(3(z0)))), 2'(3(z0)))
0'(1(2(z0))) → c5(0'(1(3(4(2(3(z0)))))), 2'(3(z0)))
0'(5(2(z0))) → c6(0'(2(4(5(3(z0))))), 2'(4(5(3(z0)))))
0'(5(2(z0))) → c7(2'(3(0(4(z0)))), 0'(4(z0)))
0'(1(2(1(z0)))) → c8(0'(2(1(z0))), 2'(1(z0)))
0'(1(3(1(z0)))) → c9(0'(3(1(1(z0)))))
0'(1(3(1(z0)))) → c10(0'(3(4(2(1(z0))))), 2'(1(z0)))
0'(1(5(1(z0)))) → c11(0'(3(1(1(z0)))))
0'(2(1(2(z0)))) → c12(0'(2(2(1(5(z0))))), 2'(2(1(5(z0)))), 2'(1(5(z0))))
0'(2(5(1(z0)))) → c13(0'(2(1(z0))), 2'(1(z0)))
0'(5(3(1(z0)))) → c14(0'(1(4(4(3(5(z0)))))))
0'(5(5(2(z0)))) → c15(2'(3(5(0(z0)))), 0'(z0))
0'(1(3(0(1(z0))))) → c16(0'(3(1(0(1(1(z0)))))), 0'(1(1(z0))))
0'(2(4(3(1(z0))))) → c17(2'(3(0(z0))), 0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(2(5(3(1(z0))))) → c19(0'(2(3(5(1(z0))))), 2'(3(5(1(z0)))))
2'(0(1(z0))) → c20(0'(2(1(z0))), 2'(1(z0)))
2'(0(1(z0))) → c21(0'(2(1(1(4(z0))))), 2'(1(1(4(z0)))))
2'(0(1(z0))) → c22(0'(3(2(4(1(z0))))), 2'(4(1(z0))))
2'(0(1(z0))) → c23(0'(2(1(4(z0)))), 2'(1(4(z0))))
2'(0(1(z0))) → c24(0'(2(2(3(4(1(z0)))))), 2'(2(3(4(1(z0))))), 2'(3(4(1(z0)))))
2'(0(1(z0))) → c25(0'(3(2(3(1(1(z0)))))), 2'(3(1(1(z0)))))
2'(0(1(z0))) → c26(0'(4(2(1(4(z0))))), 2'(1(4(z0))))
2'(5(1(z0))) → c27(0'(2(1(5(1(z0))))), 2'(1(5(1(z0)))))
2'(5(1(z0))) → c28(2'(z0))
2'(5(1(z0))) → c29(0'(2(1(4(z0)))), 2'(1(4(z0))))
2'(5(1(z0))) → c30(2'(1(4(1(z0)))))
2'(5(1(z0))) → c31(0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(5(1(z0))) → c32(2'(1(1(1(1(z0))))))
2'(0(1(2(z0)))) → c33(0'(2(3(2(1(1(z0)))))), 2'(3(2(1(1(z0))))), 2'(1(1(z0))))
2'(0(1(2(z0)))) → c34(0'(2(1(1(2(z0))))), 2'(1(1(2(z0)))), 2'(z0))
2'(0(4(1(z0)))) → c35(0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(0(5(1(z0)))) → c36(2'(1(0(z0))), 0'(z0))
2'(2(5(1(z0)))) → c37(2'(2(4(5(1(z0))))), 2'(4(5(1(z0)))))
2'(4(0(1(z0)))) → c38(0'(2(4(4(z0)))), 2'(4(4(z0))))
2'(4(0(1(z0)))) → c39(0'(0(2(4(1(z0))))), 0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(4(0(1(z0)))) → c40(0'(2(1(1(z0)))), 2'(1(1(z0))))
2'(5(2(1(z0)))) → c41(2'(2(3(1(z0)))), 2'(3(1(z0))))
2'(5(4(1(z0)))) → c42(2'(1(4(4(z0)))))
2'(5(5(1(z0)))) → c43(2'(4(5(z0))))
2'(5(5(2(z0)))) → c44(2'(3(2(z0))), 2'(z0))
2'(0(5(4(1(z0))))) → c45(0'(4(5(3(2(1(z0)))))), 2'(1(z0)))
2'(2(0(1(2(z0))))) → c46(2'(4(0(2(2(1(z0)))))), 0'(2(2(1(z0)))), 2'(2(1(z0))), 2'(1(z0)))
2'(4(0(5(1(z0))))) → c47(0'(4(2(z0))), 2'(z0))
2'(4(2(3(1(z0))))) → c48(2'(2(3(3(1(z0))))), 2'(3(3(1(z0)))))
2'(5(2(0(1(z0))))) → c49(0'(2(4(1(5(2(z0)))))), 2'(4(1(5(2(z0))))), 2'(z0))
S tuples:
0'(1(2(z0))) → c(0'(2(1(0(z0)))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c1(0'(2(3(z0))), 2'(3(z0)))
0'(1(2(z0))) → c2(0'(2(4(1(5(z0))))), 2'(4(1(5(z0)))))
0'(1(2(z0))) → c3(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c4(0'(3(2(3(z0)))), 2'(3(z0)))
0'(1(2(z0))) → c5(0'(1(3(4(2(3(z0)))))), 2'(3(z0)))
0'(5(2(z0))) → c6(0'(2(4(5(3(z0))))), 2'(4(5(3(z0)))))
0'(5(2(z0))) → c7(2'(3(0(4(z0)))), 0'(4(z0)))
0'(1(2(1(z0)))) → c8(0'(2(1(z0))), 2'(1(z0)))
0'(1(3(1(z0)))) → c9(0'(3(1(1(z0)))))
0'(1(3(1(z0)))) → c10(0'(3(4(2(1(z0))))), 2'(1(z0)))
0'(1(5(1(z0)))) → c11(0'(3(1(1(z0)))))
0'(2(1(2(z0)))) → c12(0'(2(2(1(5(z0))))), 2'(2(1(5(z0)))), 2'(1(5(z0))))
0'(2(5(1(z0)))) → c13(0'(2(1(z0))), 2'(1(z0)))
0'(5(3(1(z0)))) → c14(0'(1(4(4(3(5(z0)))))))
0'(5(5(2(z0)))) → c15(2'(3(5(0(z0)))), 0'(z0))
0'(1(3(0(1(z0))))) → c16(0'(3(1(0(1(1(z0)))))), 0'(1(1(z0))))
0'(2(4(3(1(z0))))) → c17(2'(3(0(z0))), 0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(2(5(3(1(z0))))) → c19(0'(2(3(5(1(z0))))), 2'(3(5(1(z0)))))
2'(0(1(z0))) → c20(0'(2(1(z0))), 2'(1(z0)))
2'(0(1(z0))) → c21(0'(2(1(1(4(z0))))), 2'(1(1(4(z0)))))
2'(0(1(z0))) → c22(0'(3(2(4(1(z0))))), 2'(4(1(z0))))
2'(0(1(z0))) → c23(0'(2(1(4(z0)))), 2'(1(4(z0))))
2'(0(1(z0))) → c24(0'(2(2(3(4(1(z0)))))), 2'(2(3(4(1(z0))))), 2'(3(4(1(z0)))))
2'(0(1(z0))) → c25(0'(3(2(3(1(1(z0)))))), 2'(3(1(1(z0)))))
2'(0(1(z0))) → c26(0'(4(2(1(4(z0))))), 2'(1(4(z0))))
2'(5(1(z0))) → c27(0'(2(1(5(1(z0))))), 2'(1(5(1(z0)))))
2'(5(1(z0))) → c28(2'(z0))
2'(5(1(z0))) → c29(0'(2(1(4(z0)))), 2'(1(4(z0))))
2'(5(1(z0))) → c30(2'(1(4(1(z0)))))
2'(5(1(z0))) → c31(0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(5(1(z0))) → c32(2'(1(1(1(1(z0))))))
2'(0(1(2(z0)))) → c33(0'(2(3(2(1(1(z0)))))), 2'(3(2(1(1(z0))))), 2'(1(1(z0))))
2'(0(1(2(z0)))) → c34(0'(2(1(1(2(z0))))), 2'(1(1(2(z0)))), 2'(z0))
2'(0(4(1(z0)))) → c35(0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(0(5(1(z0)))) → c36(2'(1(0(z0))), 0'(z0))
2'(2(5(1(z0)))) → c37(2'(2(4(5(1(z0))))), 2'(4(5(1(z0)))))
2'(4(0(1(z0)))) → c38(0'(2(4(4(z0)))), 2'(4(4(z0))))
2'(4(0(1(z0)))) → c39(0'(0(2(4(1(z0))))), 0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(4(0(1(z0)))) → c40(0'(2(1(1(z0)))), 2'(1(1(z0))))
2'(5(2(1(z0)))) → c41(2'(2(3(1(z0)))), 2'(3(1(z0))))
2'(5(4(1(z0)))) → c42(2'(1(4(4(z0)))))
2'(5(5(1(z0)))) → c43(2'(4(5(z0))))
2'(5(5(2(z0)))) → c44(2'(3(2(z0))), 2'(z0))
2'(0(5(4(1(z0))))) → c45(0'(4(5(3(2(1(z0)))))), 2'(1(z0)))
2'(2(0(1(2(z0))))) → c46(2'(4(0(2(2(1(z0)))))), 0'(2(2(1(z0)))), 2'(2(1(z0))), 2'(1(z0)))
2'(4(0(5(1(z0))))) → c47(0'(4(2(z0))), 2'(z0))
2'(4(2(3(1(z0))))) → c48(2'(2(3(3(1(z0))))), 2'(3(3(1(z0)))))
2'(5(2(0(1(z0))))) → c49(0'(2(4(1(5(2(z0)))))), 2'(4(1(5(2(z0))))), 2'(z0))
K tuples:none
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
0', 2'
Compound Symbols:
c, c1, c2, c3, c4, c5, c6, c7, c8, c9, c10, c11, c12, c13, c14, c15, c16, c17, c18, c19, c20, c21, c22, c23, c24, c25, c26, c27, c28, c29, c30, c31, c32, c33, c34, c35, c36, c37, c38, c39, c40, c41, c42, c43, c44, c45, c46, c47, c48, c49
(3) CdtUnreachableProof (EQUIVALENT transformation)
The following tuples could be removed as they are not reachable from basic start terms:
0'(2(5(1(z0)))) → c13(0'(2(1(z0))), 2'(1(z0)))
2'(0(1(2(z0)))) → c33(0'(2(3(2(1(1(z0)))))), 2'(3(2(1(1(z0))))), 2'(1(1(z0))))
2'(0(1(2(z0)))) → c34(0'(2(1(1(2(z0))))), 2'(1(1(2(z0)))), 2'(z0))
2'(2(5(1(z0)))) → c37(2'(2(4(5(1(z0))))), 2'(4(5(1(z0)))))
2'(2(0(1(2(z0))))) → c46(2'(4(0(2(2(1(z0)))))), 0'(2(2(1(z0)))), 2'(2(1(z0))), 2'(1(z0)))
2'(5(2(0(1(z0))))) → c49(0'(2(4(1(5(2(z0)))))), 2'(4(1(5(2(z0))))), 2'(z0))
(4) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
0'(1(3(1(z0)))) → c9(0'(3(1(1(z0)))))
0'(1(3(1(z0)))) → c10(0'(3(4(2(1(z0))))), 2'(1(z0)))
0'(1(5(1(z0)))) → c11(0'(3(1(1(z0)))))
0'(5(3(1(z0)))) → c14(0'(1(4(4(3(5(z0)))))))
2'(5(1(z0))) → c27(0'(2(1(5(1(z0))))), 2'(1(5(1(z0)))))
2'(5(1(z0))) → c28(2'(z0))
2'(5(1(z0))) → c29(0'(2(1(4(z0)))), 2'(1(4(z0))))
2'(5(1(z0))) → c30(2'(1(4(1(z0)))))
2'(5(1(z0))) → c31(0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(5(1(z0))) → c32(2'(1(1(1(1(z0))))))
2'(5(4(1(z0)))) → c42(2'(1(4(4(z0)))))
2'(5(5(1(z0)))) → c43(2'(4(5(z0))))
2'(0(1(z0))) → c20(0'(2(1(z0))), 2'(1(z0)))
2'(0(1(z0))) → c21(0'(2(1(1(4(z0))))), 2'(1(1(4(z0)))))
2'(0(1(z0))) → c22(0'(3(2(4(1(z0))))), 2'(4(1(z0))))
2'(0(1(z0))) → c23(0'(2(1(4(z0)))), 2'(1(4(z0))))
2'(0(1(z0))) → c24(0'(2(2(3(4(1(z0)))))), 2'(2(3(4(1(z0))))), 2'(3(4(1(z0)))))
2'(0(1(z0))) → c25(0'(3(2(3(1(1(z0)))))), 2'(3(1(1(z0)))))
2'(0(1(z0))) → c26(0'(4(2(1(4(z0))))), 2'(1(4(z0))))
2'(0(4(1(z0)))) → c35(0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(0(5(1(z0)))) → c36(2'(1(0(z0))), 0'(z0))
2'(4(0(1(z0)))) → c38(0'(2(4(4(z0)))), 2'(4(4(z0))))
2'(4(0(1(z0)))) → c39(0'(0(2(4(1(z0))))), 0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(4(0(1(z0)))) → c40(0'(2(1(1(z0)))), 2'(1(1(z0))))
2'(5(2(1(z0)))) → c41(2'(2(3(1(z0)))), 2'(3(1(z0))))
2'(5(5(2(z0)))) → c44(2'(3(2(z0))), 2'(z0))
2'(0(5(4(1(z0))))) → c45(0'(4(5(3(2(1(z0)))))), 2'(1(z0)))
2'(4(0(5(1(z0))))) → c47(0'(4(2(z0))), 2'(z0))
2'(4(2(3(1(z0))))) → c48(2'(2(3(3(1(z0))))), 2'(3(3(1(z0)))))
0'(1(2(z0))) → c(0'(2(1(0(z0)))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c1(0'(2(3(z0))), 2'(3(z0)))
0'(1(2(z0))) → c2(0'(2(4(1(5(z0))))), 2'(4(1(5(z0)))))
0'(1(2(z0))) → c3(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c4(0'(3(2(3(z0)))), 2'(3(z0)))
0'(1(2(z0))) → c5(0'(1(3(4(2(3(z0)))))), 2'(3(z0)))
0'(5(2(z0))) → c6(0'(2(4(5(3(z0))))), 2'(4(5(3(z0)))))
0'(5(2(z0))) → c7(2'(3(0(4(z0)))), 0'(4(z0)))
0'(1(2(1(z0)))) → c8(0'(2(1(z0))), 2'(1(z0)))
0'(2(1(2(z0)))) → c12(0'(2(2(1(5(z0))))), 2'(2(1(5(z0)))), 2'(1(5(z0))))
0'(5(5(2(z0)))) → c15(2'(3(5(0(z0)))), 0'(z0))
0'(1(3(0(1(z0))))) → c16(0'(3(1(0(1(1(z0)))))), 0'(1(1(z0))))
0'(2(4(3(1(z0))))) → c17(2'(3(0(z0))), 0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(2(5(3(1(z0))))) → c19(0'(2(3(5(1(z0))))), 2'(3(5(1(z0)))))
S tuples:
0'(1(2(z0))) → c(0'(2(1(0(z0)))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c1(0'(2(3(z0))), 2'(3(z0)))
0'(1(2(z0))) → c2(0'(2(4(1(5(z0))))), 2'(4(1(5(z0)))))
0'(1(2(z0))) → c3(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c4(0'(3(2(3(z0)))), 2'(3(z0)))
0'(1(2(z0))) → c5(0'(1(3(4(2(3(z0)))))), 2'(3(z0)))
0'(5(2(z0))) → c6(0'(2(4(5(3(z0))))), 2'(4(5(3(z0)))))
0'(5(2(z0))) → c7(2'(3(0(4(z0)))), 0'(4(z0)))
0'(1(2(1(z0)))) → c8(0'(2(1(z0))), 2'(1(z0)))
0'(1(3(1(z0)))) → c9(0'(3(1(1(z0)))))
0'(1(3(1(z0)))) → c10(0'(3(4(2(1(z0))))), 2'(1(z0)))
0'(1(5(1(z0)))) → c11(0'(3(1(1(z0)))))
0'(2(1(2(z0)))) → c12(0'(2(2(1(5(z0))))), 2'(2(1(5(z0)))), 2'(1(5(z0))))
0'(5(3(1(z0)))) → c14(0'(1(4(4(3(5(z0)))))))
0'(5(5(2(z0)))) → c15(2'(3(5(0(z0)))), 0'(z0))
0'(1(3(0(1(z0))))) → c16(0'(3(1(0(1(1(z0)))))), 0'(1(1(z0))))
0'(2(4(3(1(z0))))) → c17(2'(3(0(z0))), 0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(2(5(3(1(z0))))) → c19(0'(2(3(5(1(z0))))), 2'(3(5(1(z0)))))
2'(0(1(z0))) → c20(0'(2(1(z0))), 2'(1(z0)))
2'(0(1(z0))) → c21(0'(2(1(1(4(z0))))), 2'(1(1(4(z0)))))
2'(0(1(z0))) → c22(0'(3(2(4(1(z0))))), 2'(4(1(z0))))
2'(0(1(z0))) → c23(0'(2(1(4(z0)))), 2'(1(4(z0))))
2'(0(1(z0))) → c24(0'(2(2(3(4(1(z0)))))), 2'(2(3(4(1(z0))))), 2'(3(4(1(z0)))))
2'(0(1(z0))) → c25(0'(3(2(3(1(1(z0)))))), 2'(3(1(1(z0)))))
2'(0(1(z0))) → c26(0'(4(2(1(4(z0))))), 2'(1(4(z0))))
2'(5(1(z0))) → c27(0'(2(1(5(1(z0))))), 2'(1(5(1(z0)))))
2'(5(1(z0))) → c28(2'(z0))
2'(5(1(z0))) → c29(0'(2(1(4(z0)))), 2'(1(4(z0))))
2'(5(1(z0))) → c30(2'(1(4(1(z0)))))
2'(5(1(z0))) → c31(0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(5(1(z0))) → c32(2'(1(1(1(1(z0))))))
2'(0(4(1(z0)))) → c35(0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(0(5(1(z0)))) → c36(2'(1(0(z0))), 0'(z0))
2'(4(0(1(z0)))) → c38(0'(2(4(4(z0)))), 2'(4(4(z0))))
2'(4(0(1(z0)))) → c39(0'(0(2(4(1(z0))))), 0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(4(0(1(z0)))) → c40(0'(2(1(1(z0)))), 2'(1(1(z0))))
2'(5(2(1(z0)))) → c41(2'(2(3(1(z0)))), 2'(3(1(z0))))
2'(5(4(1(z0)))) → c42(2'(1(4(4(z0)))))
2'(5(5(1(z0)))) → c43(2'(4(5(z0))))
2'(5(5(2(z0)))) → c44(2'(3(2(z0))), 2'(z0))
2'(0(5(4(1(z0))))) → c45(0'(4(5(3(2(1(z0)))))), 2'(1(z0)))
2'(4(0(5(1(z0))))) → c47(0'(4(2(z0))), 2'(z0))
2'(4(2(3(1(z0))))) → c48(2'(2(3(3(1(z0))))), 2'(3(3(1(z0)))))
K tuples:none
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
0', 2'
Compound Symbols:
c9, c10, c11, c14, c27, c28, c29, c30, c31, c32, c42, c43, c20, c21, c22, c23, c24, c25, c26, c35, c36, c38, c39, c40, c41, c44, c45, c47, c48, c, c1, c2, c3, c4, c5, c6, c7, c8, c12, c15, c16, c17, c18, c19
(5) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)
Removed 35 of 44 dangling nodes:
0'(1(2(z0))) → c1(0'(2(3(z0))), 2'(3(z0)))
0'(1(2(z0))) → c2(0'(2(4(1(5(z0))))), 2'(4(1(5(z0)))))
0'(1(2(z0))) → c4(0'(3(2(3(z0)))), 2'(3(z0)))
0'(1(2(z0))) → c5(0'(1(3(4(2(3(z0)))))), 2'(3(z0)))
0'(5(2(z0))) → c6(0'(2(4(5(3(z0))))), 2'(4(5(3(z0)))))
0'(5(2(z0))) → c7(2'(3(0(4(z0)))), 0'(4(z0)))
0'(1(2(1(z0)))) → c8(0'(2(1(z0))), 2'(1(z0)))
0'(1(3(1(z0)))) → c9(0'(3(1(1(z0)))))
0'(1(3(1(z0)))) → c10(0'(3(4(2(1(z0))))), 2'(1(z0)))
0'(1(5(1(z0)))) → c11(0'(3(1(1(z0)))))
0'(2(1(2(z0)))) → c12(0'(2(2(1(5(z0))))), 2'(2(1(5(z0)))), 2'(1(5(z0))))
0'(5(3(1(z0)))) → c14(0'(1(4(4(3(5(z0)))))))
0'(1(3(0(1(z0))))) → c16(0'(3(1(0(1(1(z0)))))), 0'(1(1(z0))))
2'(0(1(z0))) → c20(0'(2(1(z0))), 2'(1(z0)))
0'(2(5(3(1(z0))))) → c19(0'(2(3(5(1(z0))))), 2'(3(5(1(z0)))))
2'(0(1(z0))) → c22(0'(3(2(4(1(z0))))), 2'(4(1(z0))))
2'(0(1(z0))) → c21(0'(2(1(1(4(z0))))), 2'(1(1(4(z0)))))
2'(0(1(z0))) → c24(0'(2(2(3(4(1(z0)))))), 2'(2(3(4(1(z0))))), 2'(3(4(1(z0)))))
2'(0(1(z0))) → c23(0'(2(1(4(z0)))), 2'(1(4(z0))))
2'(0(1(z0))) → c26(0'(4(2(1(4(z0))))), 2'(1(4(z0))))
2'(0(1(z0))) → c25(0'(3(2(3(1(1(z0)))))), 2'(3(1(1(z0)))))
2'(5(1(z0))) → c27(0'(2(1(5(1(z0))))), 2'(1(5(1(z0)))))
2'(5(1(z0))) → c30(2'(1(4(1(z0)))))
2'(5(1(z0))) → c29(0'(2(1(4(z0)))), 2'(1(4(z0))))
2'(5(1(z0))) → c31(0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(5(1(z0))) → c32(2'(1(1(1(1(z0))))))
2'(4(0(1(z0)))) → c38(0'(2(4(4(z0)))), 2'(4(4(z0))))
2'(0(4(1(z0)))) → c35(0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(5(2(1(z0)))) → c41(2'(2(3(1(z0)))), 2'(3(1(z0))))
2'(5(4(1(z0)))) → c42(2'(1(4(4(z0)))))
2'(4(0(1(z0)))) → c39(0'(0(2(4(1(z0))))), 0'(2(4(1(z0)))), 2'(4(1(z0))))
2'(4(0(1(z0)))) → c40(0'(2(1(1(z0)))), 2'(1(1(z0))))
2'(0(5(4(1(z0))))) → c45(0'(4(5(3(2(1(z0)))))), 2'(1(z0)))
2'(5(5(1(z0)))) → c43(2'(4(5(z0))))
2'(4(2(3(1(z0))))) → c48(2'(2(3(3(1(z0))))), 2'(3(3(1(z0)))))
(6) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c36(2'(1(0(z0))), 0'(z0))
2'(5(5(2(z0)))) → c44(2'(3(2(z0))), 2'(z0))
2'(4(0(5(1(z0))))) → c47(0'(4(2(z0))), 2'(z0))
0'(1(2(z0))) → c(0'(2(1(0(z0)))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c3(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(5(5(2(z0)))) → c15(2'(3(5(0(z0)))), 0'(z0))
0'(2(4(3(1(z0))))) → c17(2'(3(0(z0))), 0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
S tuples:
0'(1(2(z0))) → c(0'(2(1(0(z0)))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c3(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(5(5(2(z0)))) → c15(2'(3(5(0(z0)))), 0'(z0))
0'(2(4(3(1(z0))))) → c17(2'(3(0(z0))), 0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c36(2'(1(0(z0))), 0'(z0))
2'(5(5(2(z0)))) → c44(2'(3(2(z0))), 2'(z0))
2'(4(0(5(1(z0))))) → c47(0'(4(2(z0))), 2'(z0))
K tuples:none
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
2', 0'
Compound Symbols:
c28, c36, c44, c47, c, c3, c15, c17, c18
(7) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)
Split RHS of tuples not part of any SCC
(8) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(5(5(2(z0)))) → c44(2'(3(2(z0))), 2'(z0))
2'(4(0(5(1(z0))))) → c47(0'(4(2(z0))), 2'(z0))
0'(1(2(z0))) → c(0'(2(1(0(z0)))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c3(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(5(5(2(z0)))) → c15(2'(3(5(0(z0)))), 0'(z0))
0'(2(4(3(1(z0))))) → c17(2'(3(0(z0))), 0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
2'(0(5(1(z0)))) → c1(2'(1(0(z0))))
2'(0(5(1(z0)))) → c1(0'(z0))
S tuples:
0'(1(2(z0))) → c(0'(2(1(0(z0)))), 2'(1(0(z0))), 0'(z0))
0'(1(2(z0))) → c3(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
0'(5(5(2(z0)))) → c15(2'(3(5(0(z0)))), 0'(z0))
0'(2(4(3(1(z0))))) → c17(2'(3(0(z0))), 0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(3(2(1(0(z0))))), 2'(1(0(z0))), 0'(z0))
2'(5(1(z0))) → c28(2'(z0))
2'(5(5(2(z0)))) → c44(2'(3(2(z0))), 2'(z0))
2'(4(0(5(1(z0))))) → c47(0'(4(2(z0))), 2'(z0))
2'(0(5(1(z0)))) → c1(2'(1(0(z0))))
2'(0(5(1(z0)))) → c1(0'(z0))
K tuples:none
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
2', 0'
Compound Symbols:
c28, c44, c47, c, c3, c15, c17, c18, c1
(9) CdtGraphRemoveTrailingProof (BOTH BOUNDS(ID, ID) transformation)
Removed 11 trailing tuple parts
(10) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
S tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
K tuples:none
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
2', 0'
Compound Symbols:
c28, c1, c44, c47, c, c3, c15, c17, c18, c1
(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
We considered the (Usable) Rules:none
And the Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [3] + [2]x1
POL(0'(x1)) = [2] + x1
POL(1(x1)) = x1
POL(2(x1)) = [2] + x1
POL(2'(x1)) = [1] + [2]x1
POL(3(x1)) = x1
POL(4(x1)) = x1
POL(5(x1)) = x1
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c28(x1)) = x1
POL(c3(x1)) = x1
POL(c44(x1)) = x1
POL(c47(x1)) = x1
(12) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
S tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
K tuples:
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
2', 0'
Compound Symbols:
c28, c1, c44, c47, c, c3, c15, c17, c18, c1
(13) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
We considered the (Usable) Rules:none
And the Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [3] + [4]x1
POL(0'(x1)) = [3]
POL(1(x1)) = x1
POL(2(x1)) = [5] + [2]x1
POL(2'(x1)) = [4] + [4]x1
POL(3(x1)) = 0
POL(4(x1)) = [4] + x1
POL(5(x1)) = [2] + x1
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c28(x1)) = x1
POL(c3(x1)) = x1
POL(c44(x1)) = x1
POL(c47(x1)) = x1
(14) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
S tuples:
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
K tuples:
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
2', 0'
Compound Symbols:
c28, c1, c44, c47, c, c3, c15, c17, c18, c1
(15) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
2'(0(5(1(z0)))) → c1
We considered the (Usable) Rules:none
And the Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [4] + [3]x1
POL(0'(x1)) = [2]
POL(1(x1)) = [2]
POL(2(x1)) = [1]
POL(2'(x1)) = [4]
POL(3(x1)) = [5]
POL(4(x1)) = [3]
POL(5(x1)) = [3]
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c28(x1)) = x1
POL(c3(x1)) = x1
POL(c44(x1)) = x1
POL(c47(x1)) = x1
(16) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
S tuples:
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
K tuples:
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(0(5(1(z0)))) → c1
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
2', 0'
Compound Symbols:
c28, c1, c44, c47, c, c3, c15, c17, c18, c1
(17) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
2'(5(5(2(z0)))) → c44(2'(z0))
We considered the (Usable) Rules:none
And the Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [4]x1
POL(0'(x1)) = 0
POL(1(x1)) = x1
POL(2(x1)) = [5] + [2]x1
POL(2'(x1)) = [4]x1
POL(3(x1)) = 0
POL(4(x1)) = x1
POL(5(x1)) = x1
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c28(x1)) = x1
POL(c3(x1)) = x1
POL(c44(x1)) = x1
POL(c47(x1)) = x1
(18) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
S tuples:
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
K tuples:
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(0(5(1(z0)))) → c1
2'(5(5(2(z0)))) → c44(2'(z0))
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
2', 0'
Compound Symbols:
c28, c1, c44, c47, c, c3, c15, c17, c18, c1
(19) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
2'(4(0(5(1(z0))))) → c47(2'(z0))
We considered the (Usable) Rules:none
And the Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [4]x1
POL(0'(x1)) = [3]
POL(1(x1)) = x1
POL(2(x1)) = [4]x1
POL(2'(x1)) = x1
POL(3(x1)) = [1]
POL(4(x1)) = x1
POL(5(x1)) = [4] + x1
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c28(x1)) = x1
POL(c3(x1)) = x1
POL(c44(x1)) = x1
POL(c47(x1)) = x1
(20) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
S tuples:
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
K tuples:
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(0(5(1(z0)))) → c1
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
2', 0'
Compound Symbols:
c28, c1, c44, c47, c, c3, c15, c17, c18, c1
(21) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
We considered the (Usable) Rules:none
And the Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [2]x1
POL(0'(x1)) = [3] + [3]x1
POL(1(x1)) = x1
POL(2(x1)) = [1] + [4]x1
POL(2'(x1)) = [4] + [2]x1
POL(3(x1)) = x1
POL(4(x1)) = x1
POL(5(x1)) = [5] + x1
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c28(x1)) = x1
POL(c3(x1)) = x1
POL(c44(x1)) = x1
POL(c47(x1)) = x1
(22) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
S tuples:
0'(2(4(3(1(z0))))) → c18(0'(z0))
K tuples:
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(0(5(1(z0)))) → c1
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
2', 0'
Compound Symbols:
c28, c1, c44, c47, c, c3, c15, c17, c18, c1
(23) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)
Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.
0'(2(4(3(1(z0))))) → c18(0'(z0))
We considered the (Usable) Rules:none
And the Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
The order we found is given by the following interpretation:
Polynomial interpretation :
POL(0(x1)) = [4]x1
POL(0'(x1)) = [2] + [2]x1
POL(1(x1)) = x1
POL(2(x1)) = [1] + [4]x1
POL(2'(x1)) = [4]x1
POL(3(x1)) = x1
POL(4(x1)) = x1
POL(5(x1)) = [3] + x1
POL(c(x1)) = x1
POL(c1) = 0
POL(c1(x1)) = x1
POL(c15(x1)) = x1
POL(c17(x1)) = x1
POL(c18(x1)) = x1
POL(c28(x1)) = x1
POL(c3(x1)) = x1
POL(c44(x1)) = x1
POL(c47(x1)) = x1
(24) Obligation:
Complexity Dependency Tuples Problem
Rules:
0(1(2(z0))) → 0(2(1(0(z0))))
0(1(2(z0))) → 1(0(2(3(z0))))
0(1(2(z0))) → 0(2(4(1(5(z0)))))
0(1(2(z0))) → 0(3(2(1(0(z0)))))
0(1(2(z0))) → 1(0(3(2(3(z0)))))
0(1(2(z0))) → 0(1(3(4(2(3(z0))))))
0(5(2(z0))) → 0(2(4(5(3(z0)))))
0(5(2(z0))) → 5(4(2(3(0(4(z0))))))
0(1(2(1(z0)))) → 3(1(4(0(2(1(z0))))))
0(1(3(1(z0)))) → 5(0(3(1(1(z0)))))
0(1(3(1(z0)))) → 1(0(3(4(2(1(z0))))))
0(1(5(1(z0)))) → 5(0(3(1(1(z0)))))
0(2(1(2(z0)))) → 0(2(2(1(5(z0)))))
0(2(5(1(z0)))) → 1(1(5(0(2(1(z0))))))
0(5(3(1(z0)))) → 0(1(4(4(3(5(z0))))))
0(5(5(2(z0)))) → 5(4(2(3(5(0(z0))))))
0(1(3(0(1(z0))))) → 0(3(1(0(1(1(z0))))))
0(2(4(3(1(z0))))) → 1(3(4(2(3(0(z0))))))
0(2(4(3(1(z0))))) → 4(0(3(2(1(0(z0))))))
0(2(5(3(1(z0))))) → 5(0(2(3(5(1(z0))))))
2(0(1(z0))) → 3(0(2(1(z0))))
2(0(1(z0))) → 0(2(1(1(4(z0)))))
2(0(1(z0))) → 0(3(2(4(1(z0)))))
2(0(1(z0))) → 3(0(2(1(4(z0)))))
2(0(1(z0))) → 0(2(2(3(4(1(z0))))))
2(0(1(z0))) → 0(3(2(3(1(1(z0))))))
2(0(1(z0))) → 4(0(4(2(1(4(z0))))))
2(5(1(z0))) → 0(2(1(5(1(z0)))))
2(5(1(z0))) → 1(4(5(4(2(z0)))))
2(5(1(z0))) → 5(0(2(1(4(z0)))))
2(5(1(z0))) → 5(2(1(4(1(z0)))))
2(5(1(z0))) → 1(5(0(2(4(1(z0))))))
2(5(1(z0))) → 5(2(1(1(1(1(z0))))))
2(0(1(2(z0)))) → 0(2(3(2(1(1(z0))))))
2(0(1(2(z0)))) → 4(0(2(1(1(2(z0))))))
2(0(4(1(z0)))) → 3(0(2(4(1(z0)))))
2(0(5(1(z0)))) → 5(4(2(1(0(z0)))))
2(2(5(1(z0)))) → 3(2(2(4(5(1(z0))))))
2(4(0(1(z0)))) → 1(0(2(4(4(z0)))))
2(4(0(1(z0)))) → 3(0(0(2(4(1(z0))))))
2(4(0(1(z0)))) → 5(4(0(2(1(1(z0))))))
2(5(2(1(z0)))) → 1(5(2(2(3(1(z0))))))
2(5(4(1(z0)))) → 4(5(2(1(4(4(z0))))))
2(5(5(1(z0)))) → 1(5(4(2(4(5(z0))))))
2(5(5(2(z0)))) → 5(5(2(3(2(z0)))))
2(0(5(4(1(z0))))) → 0(4(5(3(2(1(z0))))))
2(2(0(1(2(z0))))) → 2(4(0(2(2(1(z0))))))
2(4(0(5(1(z0))))) → 1(4(5(0(4(2(z0))))))
2(4(2(3(1(z0))))) → 4(2(2(3(3(1(z0))))))
2(5(2(0(1(z0))))) → 0(2(4(1(5(2(z0))))))
Tuples:
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
2'(0(5(1(z0)))) → c1
S tuples:none
K tuples:
0'(5(5(2(z0)))) → c15(0'(z0))
0'(2(4(3(1(z0))))) → c17(0'(z0))
2'(5(1(z0))) → c28(2'(z0))
2'(0(5(1(z0)))) → c1(0'(z0))
2'(0(5(1(z0)))) → c1
2'(5(5(2(z0)))) → c44(2'(z0))
2'(4(0(5(1(z0))))) → c47(2'(z0))
0'(1(2(z0))) → c(0'(z0))
0'(1(2(z0))) → c3(0'(z0))
0'(2(4(3(1(z0))))) → c18(0'(z0))
Defined Rule Symbols:
0, 2
Defined Pair Symbols:
2', 0'
Compound Symbols:
c28, c1, c44, c47, c, c3, c15, c17, c18, c1
(25) SIsEmptyProof (EQUIVALENT transformation)
The set S is empty
(26) BOUNDS(O(1), O(1))